PRISM

Benchmark
Model:firewire-pta v.1 (PTA)
Parameter(s)delay = 30, T = 5000
Property:deadline (prob-reach-time-bounded)
Invocation (default)
./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 firewire-pta.prism firewire-pta.props --property deadline -const delay=30,T=5000
Execution
Walltime:7.122632026672363s
Return code:0
Note(s):Correctness of result is not checked because no reference result is available.
Log
PRISM
=====

Version: 4.5.dev
Date: Sun Mar 15 03:29:19 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 firewire-pta.prism firewire-pta.props --property deadline -const 'delay=30,T=5000'

Parsing model file "firewire-pta.prism"...

Type:        PTA
Modules:     wire12 node1 wire21 node2 
Variables:   w12 y1 y2 x1 s1 w21 z1 z2 x2 s2 

Parsing properties file "firewire-pta.props"...

2 properties:
(1) "deadline": Pmin=? [ F<=T "done" ]
(2) "eventually": Pmin=? [ F "done" ]

---------------------------------------------------------------------

Model checking: "deadline": Pmin=? [ F<=T "done" ]
Model constants: delay=30
Property constants: T=5000

Building PTA...

PTA: 6 clocks, 65 locations, 127 transitions
Target (s1=8&s2=7|s1=7&s2=8) satisfied by 4 locations.
Modifying PTA to encode time bound from property...
New PTA: 7 clocks, 66 locations, 135 transitions

Building initial STPG...

Building forwards reachability graph... 3469 states
Graph constructed in 0.193 secs.
Graph: 3469 symbolic states (1 initial, 130 target)

Model checking STPG...
STPG model checked in 0.28 secs.
2634/3469 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
42 refineable states.

Refinement 1...
42 states successfully refined in 0.217 secs.
180+0=180 states of STPG rebuilt in 0.0 secs.
New STPG has 3511 states.

Model checking STPG...
STPG model checked in 0.155 secs.
2718/3511 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
96 refineable states.

Refinement 2...
96 states successfully refined in 0.359 secs.
288+0=288 states of STPG rebuilt in 0.0 secs.
New STPG has 3607 states.

Model checking STPG...
STPG model checked in 0.175 secs.
2910/3607 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
36 refineable states.

Refinement 3...
36 states successfully refined in 0.094 secs.
132+0=132 states of STPG rebuilt in 0.0 secs.
New STPG has 3643 states.

Model checking STPG...
STPG model checked in 0.093 secs.
2982/3643 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
60 refineable states.

Refinement 4...
60 states successfully refined in 0.119 secs.
180+0=180 states of STPG rebuilt in 0.0 secs.
New STPG has 3703 states.

Model checking STPG...
STPG model checked in 0.106 secs.
3102/3703 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
60 refineable states.

Refinement 5...
60 states successfully refined in 0.114 secs.
162+0=162 states of STPG rebuilt in 0.0 secs.
New STPG has 3763 states.

Model checking STPG...
STPG model checked in 0.075 secs.
3222/3763 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
42 refineable states.

Refinement 6...
42 states successfully refined in 0.072 secs.
108+0=108 states of STPG rebuilt in 0.0 secs.
New STPG has 3805 states.

Model checking STPG...
STPG model checked in 0.069 secs.
3306/3805 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
24 refineable states.

Refinement 7...
24 states successfully refined in 0.043 secs.
75+0=75 states of STPG rebuilt in 0.0 secs.
New STPG has 3829 states.

Model checking STPG...
STPG model checked in 0.067 secs.
3354/3829 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
27 refineable states.

Refinement 8...
27 states successfully refined in 0.071 secs.
66+0=66 states of STPG rebuilt in 0.0 secs.
New STPG has 3856 states.

Model checking STPG...
STPG model checked in 0.064 secs.
3408/3856 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
12 refineable states.

Refinement 9...
12 states successfully refined in 0.042 secs.
42+0=42 states of STPG rebuilt in 0.0 secs.
New STPG has 3880 states.

Model checking STPG...
STPG model checked in 0.073 secs.
3444/3880 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
6 refineable states.

Refinement 10...
6 states successfully refined in 0.089 secs.
58+0=58 states of STPG rebuilt in 0.0 secs.
New STPG has 3892 states.

Model checking STPG...
STPG model checked in 0.072 secs.
3462/3892 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.

Refinement 11...
40 states successfully refined in 0.283 secs.
160+0=160 states of STPG rebuilt in 0.0 secs.
New STPG has 3972 states.

Model checking STPG...
STPG model checked in 0.071 secs.
3582/3972 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.

Refinement 12...
40 states successfully refined in 0.319 secs.
144+0=144 states of STPG rebuilt in 0.0 secs.
New STPG has 4036 states.

Model checking STPG...
STPG model checked in 0.067 secs.
3686/4036 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.

Refinement 13...
40 states successfully refined in 0.148 secs.
132+0=132 states of STPG rebuilt in 0.0 secs.
New STPG has 4100 states.

Model checking STPG...
STPG model checked in 0.075 secs.
3790/4100 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
28 refineable states.

Refinement 14...
28 states successfully refined in 0.118 secs.
88+0=88 states of STPG rebuilt in 0.0 secs.
New STPG has 4144 states.

Model checking STPG...
STPG model checked in 0.074 secs.
3862/4144 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.25
16 refineable states.

Refinement 15...
16 states successfully refined in 0.066 secs.
60+0=60 states of STPG rebuilt in 0.0 secs.
New STPG has 4168 states.

Model checking STPG...
STPG model checked in 0.076 secs.
3902/4168 states converged.
Diff across 1 initial state: 0.041015625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.892578125
Max diff over all states: 0.25
20 refineable states.

Refinement 16...
20 states successfully refined in 0.074 secs.
68+0=68 states of STPG rebuilt in 0.0 secs.
New STPG has 4200 states.

Model checking STPG...
STPG model checked in 0.084 secs.
3950/4200 states converged.
Diff across 1 initial state: 0.041015625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.892578125
Max diff over all states: 0.15625
16 refineable states.

Refinement 17...
16 states successfully refined in 0.054 secs.
52+0=52 states of STPG rebuilt in 0.0 secs.
New STPG has 4228 states.

Model checking STPG...
STPG model checked in 0.074 secs.
3974/4228 states converged.
Diff across 1 initial state: 0.025390625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.876953125
Max diff over all states: 0.15625
8 refineable states.

Refinement 18...
6 states successfully refined in 0.092 secs.
58+0=58 states of STPG rebuilt in 0.0 secs.
New STPG has 4240 states.

Model checking STPG...
STPG model checked in 0.074 secs.
3986/4240 states converged.
Diff across 1 initial state: 0.025390625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.876953125
Max diff over all states: 0.15625
44 refineable states.

Refinement 19...
40 states successfully refined in 0.236 secs.
160+0=160 states of STPG rebuilt in 0.0 secs.
New STPG has 4320 states.

Model checking STPG...
STPG model checked in 0.077 secs.
4175/4320 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
26 refineable states.

Refinement 20...
10 states successfully refined in 0.077 secs.
36+0=36 states of STPG rebuilt in 0.0 secs.
New STPG has 4336 states.

Model checking STPG...
STPG model checked in 0.086 secs.
4201/4336 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
26 refineable states.

Refinement 21...
10 states successfully refined in 0.038 secs.
33+0=33 states of STPG rebuilt in 0.0 secs.
New STPG has 4352 states.

Model checking STPG...
STPG model checked in 0.155 secs.
4227/4352 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
23 refineable states.

Refinement 22...
7 states successfully refined in 0.037 secs.
22+0=22 states of STPG rebuilt in 0.0 secs.
New STPG has 4363 states.

Model checking STPG...
STPG model checked in 0.175 secs.
4245/4363 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.0625
20 refineable states.

Refinement 23...
4 states successfully refined in 0.018 secs.
16+0=16 states of STPG rebuilt in 0.0 secs.
New STPG has 4369 states.

Model checking STPG...
STPG model checked in 0.113 secs.
4332/4369 states converged.
Diff across 1 initial state: 0.0
Lower/upper bounds for 1 initial state: 0.8515625 - 0.8515625

Initial STPG: 3469 states (1 initial), 4982 transitions, 4620 choices, 3423 choice sets, p1max/avg = 3/0.99, p2max/avg = 2/1.35
Final STPG: 4369 states (1 initial), 8212 transitions, 7674 choices, 4756 choice sets, p1max/avg = 7/1.09, p2max/avg = 6/1.61

Terminated after 23 refinements in 6.20 secs.

Abstraction-refinement time breakdown:
* 0.94 secs (15.2%) = Building initial STPG
* 0.00 secs (0.0%) = Rebuilding STPG (23 x avg 0.00 secs)
* 2.43 secs (39.2%) = model checking STPG (24 x avg 0.10 secs) (lb=46.1%) (prob0=20.5%) (pre=92.3%) (iters=964)
* 2.78 secs (44.8%) = refinement (23 x avg 0.12 secs)

Final diff across 1 initial state: 0.0
Final lower/upper bounds for 1 initial state: 0.8515625 - 0.8515625

Model checking completed in 6.398 secs.

Result (minimum probability): 0.8515625


Overall running time: 6.936 seconds.